Lemme de Newman

En mathématiques et en informatique, plus précisément dans la théorie des relations binaires, le lemme de Newman dit qu'une relation binaire noethérienne est confluente si elle est localement confluente^[1]. Une démonstration relativement simple (induction sur une relation bien fondée) est due à Gérard Huet en 1980^[2]. La démonstration originale de Newman est plus compliquée, mais la méthode des diagrammes décroissants^[Quoi ?] montre bien comment elle fonctionne^[3].

↑ Franz Baader, Tobias Nipkow, (1998) Term Rewriting and All That, Cambridge University Press (ISBN 0-521-77920-0).
↑ Gérard Huet, « Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems », Journal of the ACM (JACM), October 1980, Volume 27, Issue 4, pp. 797 - 821.
↑ Jan Willem Klop, Vincent van Oostrom, Roel C. de Vrijer, « A geometric proof of confluence by decreasing diagrams », J. Log. Comput. 10(3): 437-460 (2000).

[1] Franz Baader, Tobias Nipkow, (1998) Term Rewriting and All That, Cambridge University Press (ISBN 0-521-77920-0).

[2] Gérard Huet, « Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems », Journal of the ACM (JACM), October 1980, Volume 27, Issue 4, pp. 797 - 821.

[3] Jan Willem Klop, Vincent van Oostrom, Roel C. de Vrijer, « A geometric proof of confluence by decreasing diagrams », J. Log. Comput. 10(3): 437-460 (2000).

[1]

[2]

[3]